theory Design_Memory
imports "../DesignSpec"

begin

section "TEEC"

definition TEEC_RegisterSharedMemoryR:: "Sys_Config ⇒ StateR ⇒ TEEC_CONTEXT_TYPE ⇒ TEEC_SharedMemory 
                                                    ⇒ (StateR × TEEC_RETURN_CODE_TYPE)" where
          "TEEC_RegisterSharedMemoryR sc s ctx shm ≡ 
                                let s'= (TEEC_RegisterSharedMemory sc (⇑s) ctx shm) in (s⇓(fst s'), (snd s'))"

definition TEEC_AllocateSharedMemoryR:: "Sys_Config ⇒ StateR ⇒ TEEC_CONTEXT_TYPE ⇒ TEEC_SharedMemory 
                                                    ⇒ (StateR × TEEC_RETURN_CODE_TYPE)" where
  "TEEC_AllocateSharedMemoryR sc s ctx shm ≡ 
                                let s'= (TEEC_AllocateSharedMemory sc (⇑s) ctx shm) in (s⇓(fst s'), (snd s'))"

definition TEEC_ReleaseSharedMemoryR :: "Sys_Config ⇒ StateR ⇒TEEC_SharedMemory ⇒ StateR " where
  "TEEC_ReleaseSharedMemoryR sc s shm ≡ 
                                let s'= (TEEC_ReleaseSharedMemory sc (⇑s) shm) in (s⇓s')"

section "TEE"

definition TEE_CheckMemoryAccessRightsR :: "Sys_Config ⇒ StateR ⇒ accessFlags ⇒ MemBlock ⇒ BUFFER_SIZE_TYPE 
                                                       ⇒ TEE_RETURN_CODE_TYPE" where
          "TEE_CheckMemoryAccessRightsR sc s aF memblock buffer_size ≡ 
                                let return_code = (TEE_CheckMemoryAccessRights sc (⇑s) aF memblock buffer_size) in return_code
"

definition TEE_MallocR :: "Sys_Config ⇒ StateR ⇒ BUFFER_SIZE_TYPE ⇒ hint ⇒ StateR" where
  "TEE_MallocR sc s buffer_size h ≡ 
                                let s'= (TEE_Malloc sc (⇑s) buffer_size h) in (s⇓s')
"

definition TEE_ReallocR :: "Sys_Config ⇒ StateR ⇒ MemBlock ⇒ BUFFER_SIZE_TYPE ⇒ StateR" where
  "TEE_ReallocR sc s memblock new_size ≡ 
                                let s'= (TEE_Realloc sc (⇑s) memblock new_size) in (s⇓s')
"

definition TEE_FreeR :: "Sys_Config ⇒ StateR ⇒ MemBlock ⇒ StateR" where
  "TEE_FreeR sc s memblock ≡
                                let s'= (TEE_Free sc (⇑s) memblock) in (s⇓s')
"

end